package br.edu.ufcg.symbolrt.examples;

import br.edu.ufcg.symbolrt.base.Action;
import br.edu.ufcg.symbolrt.base.Location;
import br.edu.ufcg.symbolrt.base.TIOSTS;
import br.edu.ufcg.symbolrt.base.TypedData;
import br.edu.ufcg.symbolrt.util.Constants;

public class ToyI2 {
	
	 public static TIOSTS createSPEC(){
		 TIOSTS tiosts = new TIOSTS("ToyI2");
		 
         // Variables
		 TypedData y = new TypedData("y", Constants.TYPE_INTEGER);
		 tiosts.addVariable(y);
         tiosts.addActionParameter(y);
         
         // There are no parameters       
         
         Action init4 = new Action("Init4", Constants.ACTION_INTERNAL);
         tiosts.addAction(init4);
         Action aInput = new Action("a", Constants.ACTION_INPUT);
         tiosts.addAction(aInput); 
         Action aOutput = new Action("a", Constants.ACTION_OUTPUT);
         tiosts.addAction(aOutput);     
         
         Action c = new Action("c", Constants.ACTION_INPUT);
         tiosts.addAction(c);   
         
         Location start4 = new Location("Start4");
         tiosts.addLocation(start4);
         Location s10 = new Location("S10");
         tiosts.addLocation(s10);
         Location s11 = new Location("S11");
         tiosts.addLocation(s11);        
         Location s12 = new Location("S12");
         tiosts.addLocation(s12);
         Location lc4 = new Location("lc4");
         tiosts.addLocation(lc4);
         
         // Initial Condition
         tiosts.setInitialCondition(Constants.GUARD_TRUE);
         
         // Initial Location
         tiosts.setInitialLocation(start4);
         
         // Transitions
         tiosts.createTransition("Start4", Constants.GUARD_TRUE, Constants.GUARD_TRUE, init4, null, null, "S10");
         tiosts.createTransition("S10", Constants.GUARD_TRUE, Constants.GUARD_TRUE, c, "y := 0", null, "S11");
         tiosts.createTransition("S11", "y > 7", Constants.GUARD_TRUE, aInput, null, null, "S12");
         tiosts.createTransition("S12", Constants.GUARD_TRUE, Constants.GUARD_TRUE, aOutput, null, null, "S12");
         tiosts.createTransition("S10", Constants.GUARD_TRUE, Constants.GUARD_TRUE, aInput, null, null, "lc4");
         tiosts.createTransition("S11", Constants.GUARD_TRUE, Constants.GUARD_TRUE, c, null, null, "lc4");
         tiosts.createTransition("S11", "y <= 7", Constants.GUARD_TRUE, aInput, null, null, "lc4");
         tiosts.createTransition("S12", Constants.GUARD_TRUE, Constants.GUARD_TRUE, aInput, null, null, "lc4");
         tiosts.createTransition("S12", Constants.GUARD_TRUE, Constants.GUARD_TRUE, c, null, null, "lc4");
         
         return tiosts;		 
	 }

}
